\begin{tabbing}
EventsWithState
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type\+
\\[0ex]$\times$ (${\it eq}$:EqDecider($E$)
\\[0ex]$\times$ ${\it pred?}$:($E$$\rightarrow$(?$E$))
\\[0ex]$\times$ ${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id)))
\\[0ex]$\times$ ${\it oaxioms}$:EOrderAxioms($E$; ${\it pred?}$; ${\it info}$)
\\[0ex]$\times$ $T$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ $V$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ ${\it init}$:($i$:Id$\rightarrow$EState($T$($i$)))
\\[0ex]$\times$ ${\it Trans}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$EState($T$($i$))$\rightarrow$EState($T$($i$)))
\\[0ex]$\times$ ${\it val}$:($e$:$E$$\rightarrow$kindcase(kind($e$); $a$.$V$(loc($e$),$a$); $l$,$t$.$M$($l$,$t$) ))
\\[0ex]$\times$ ${\it Send}$:\=($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$\+
\\[0ex](Msg($M$) List))
\-\\[0ex]$\times$ ${\it Choose}$:($i$,$a$:Id$\rightarrow\mathbb{N}\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$(?($V$($i$,$a$))))
\\[0ex]$\times$ ${\it time}$:($E$$\rightarrow\mathbb{Q}$)
\\[0ex]$\times$ (${\it va}$:\=val{-}axiom($E$;$V$;$M$;${\it info}$;${\it pred?}$;\+
\\[0ex]${\it init}$;${\it Trans}$;
\\[0ex]${\it Choose}$;${\it Send}$;${\it val}$;${\it time}$)
\-\\[0ex]$\times$ Top))
\-
\end{tabbing}